import net.sf.javabdd.BDD;
import net.sf.javabdd.BDDFactory;
import net.sf.javabdd.JFactory;


final public class BDDCreator {

	private transient BDDFactory fac;
	private transient BDD bdd;
	private transient final int[][] board;
	private transient final int[][] boardIDs;

	public BDDCreator(final int[][] newBoard, final int[][] newBoardIDs) {
		this.board = newBoard;
		this.boardIDs = newBoardIDs;
	}

	private void addRule(final int row, final int col, final BDD nthis) {
		final BDD neighbor = fac.nithVar(boardIDs[row][col]);
		final BDD newCond = nthis.or(neighbor);
		bdd = bdd.and(newCond);
	}

	private void vertical(final int row, final int col, final BDD nthis) {
		for (int colNeighbor = 0; colNeighbor < board.length; colNeighbor++) {
			if (col != colNeighbor) {
				addRule(row, colNeighbor, nthis);
			}
		}

	}

	private void horizontal(final int row, final int col, final BDD nthis) {
		for (int rowNeighbor = 0; rowNeighbor < board[0].length; rowNeighbor++) {
			if (row != rowNeighbor) {
				addRule(rowNeighbor, col, nthis);
			}
		}

	}

	private void topRightToBottomLeftDiagonal(final int row, final int col, final BDD nthis) {
		final int min = Math.min(row, col);
		int colNeighbor = col - min;
		int rowNeighbor = row - min;
		while (colNeighbor < board.length && rowNeighbor < board.length) {
			if (colNeighbor == col && rowNeighbor == row) {
				colNeighbor++;
				rowNeighbor++;
				continue;
			}
			addRule(rowNeighbor, colNeighbor, nthis);
			colNeighbor++;
			rowNeighbor++;
		}
	}

	private void bottomRightToTopLeftDiagonal(final int row, final int col, final BDD nthis) {
		int colNeighbor, rowNeighbor;
		if (row + col < board.length) {
			colNeighbor = 0;
			rowNeighbor = row + col;
		} else {
			rowNeighbor = board.length - 1;
			colNeighbor = row - (board.length - 1 - col);
		}

		while (colNeighbor < board.length && rowNeighbor >= 0) {
			if (colNeighbor == col && rowNeighbor == row) {
				colNeighbor++;
				rowNeighbor--;
				continue;
			}
			addRule(rowNeighbor, colNeighbor, nthis);
			colNeighbor++;
			rowNeighbor--;
		}
	}
	
	private void oneQueenEachRow() {
		for (int row = 0; row < board.length; row++) {
			BDD rowCond = fac.zero();
			for (int col = 0; col < board[1].length; col++) {
				final BDD slotInRow = fac.ithVar(boardIDs[row][col]);
				rowCond = rowCond.or(slotInRow);
			}
			bdd = bdd.and(rowCond);
		}
	}

	public BDD initializeBDD() {
		fac = JFactory.init(2000000, 200000);
		fac.setVarNum(board.length * board.length);
		bdd = fac.one();

		for (int row = 0; row < board.length; row++) {
			for (int col = 0; col < board[1].length; col++) {
				final BDD nthis = fac.nithVar(boardIDs[row][col]);
				vertical(row, col, nthis);
				horizontal(row, col, nthis);	
				topRightToBottomLeftDiagonal(row, col, nthis);
				bottomRightToTopLeftDiagonal(row, col, nthis);
			}
		}
		oneQueenEachRow();
		//bdd.printDot();
		return bdd;
	}

}
